perm filename RUNT[AP,JRA] blob sn#138547 filedate 1975-01-16 generic text, type T, neo UTF8
(DEFPROP PF(LAMBDA(L)(PROG NIL 
A(COND((ATOM(CAR L))(PRINC(CAR L)))
((EQ(LENGTH(CAR L))1)(PRINC(CAAR L)))
(T(PF(LIST(CAAR L)))(PRINC @/()(PF(CDAR L))(PRINC @/))))
(SETQ L(CDR L))
(COND(L(PRINC @/,)(GO A)))))
EXPR)
(SETQ NEGSGN @¬)



(DEFPROP THSET
   (LAMBDA(A B)
	(EVAL(LIST @THSETQ A(LIST @QUOTE B)T T)))
EXPR)

(DEFPROP THVSET
   (LAMBDA(A B)
	(EVAL(LIST @THVSETQ A(LIST @QUOTE B))))
EXPR)


(DEFPROP GETNUMARG
   (LAMBDA(X)
	(COND((EQ(CAR X)@#)(CAADDR X))
	     (T(CAR X)))  )
EXPR)




(DEFPROP NEWVAR
   (LAMBDA(X)
      (PROG (XT)
	(SETQ XT X)
NE1	(THSET (CAR XT)(READLIST(APPEND(LIST @X)(EXPLODE(THSETQ(THV XN)(ADD1(THV XN)))))))
	(THVAL(LIST @THASSERT(LIST @ISVAR (CAR XT)))THALIST)
	(SETQ XT(CDR XT))
	(COND(XT(GO NE1))) 
	(RETURN T)   ))
FEXPR)


(DEFPROP GZ
   (LAMBDA(X)
	(AND(NOT(MINUSP (CAR X)))(NOT(ZEROP (CAR X)))) )
EXPR)

(DEFPROP GT
   (LAMBDA(X Y)
	(*GREAT (CAR X)(CAR Y)) )
EXPR)


(DEFPROP SUB2
   (LAMBDA(X)
	(SUB1(SUB1 X))  )
EXPR)



(SETQ ADVBRL @((FOR . AD1)(DELETE . AD2)(ADD . AD3)(ALTER . AD4)(ASSUME . AD5)
	       (RESTRICT . AD6)(ADVICE . AD7)(STATUS . AD8)))


(DEFPROP ADVICESYS
   (LAMBDA NIL
      (PROG(ADV ALR NA OPT LL VN)
	(TERPRI)(PRINT @*********___ENTERING__ADVICE__SYSTEM___*********)(TERPRI)
	(SETQ SSW T)
AD01	(SETQ OPT NIL)
	(PRINT(READLIST(APPEND @(#)(EXPLODE(ADD1 AN)))))
	(SETQ ADV(READ))
	(COND((NULL ADV) (SETQ SSW NIL) (RETURN NIL)))
	(COND((EQ ADV T)(SETQ SSW NIL) (RETURN T)))
	(SETQ AN(ADD1 AN))
	(SETQ ADV(LIST ADV AN))
	(SETQ NA(ASSOC(CAR ADV)ADVBRL))
	(COND(NA(GO(CDR NA)))
	     (T(SETQ AN(SUB1 AN))(PRINT @NONESENSE!!)(GO AD01)))
AD1	(SETQ ADV(CONS(READ)ADV))
	(SETQ NA(CAR ADV))
	(SETQ ADV(CONS(READ)ADV))
	(COND((EQ @FIRST(CAR ADV))(SETQ OPT T)
	      (SETQ ADV(CONS(READ)ADV)) ))
	(SETQ ADV(CONS(CONS(READ)(READ))ADV))
	(SETQ AL(CONS(REVERSE ADV)AL))
	(COND((NULL OPT)(RPLACD(FBODY(GET NA @THEOREM))
			(LIST(LIST @THOR(CONS @THAND(CDR(FBODY(GET NA @THEOREM))))
					(LIST @THGOAL(APPEND(CAR ADV)@(R))@(THTBF FILTEROP))))))

	     (T(RPLACD(FBODY(GET NA @THEOREM))
		      (CONS(LIST @THGOAL(APPEND(CAR ADV)@(R))@(THTBF FILTEROP))
			   (CDR(FBODY(GET NA @THEOREM)))))))
	(PRINT @IS_RULE_DEFINED_FOR_GIVEN_ADVICE?*)
	(COND((READ)(GO AD01)))
AD02	(PRINT @DEFINITION_FILENAME_)(PRINC @(ENCLOSE IN PARENS PLEASE))(PRINC @*)
	(SETQ LL(READ))
	(COND((AND(NOT(NULL LL))(NOT(EQ @DSK:(CAR LL))))(SETQ FILENAME(CAR LL))(GO AD002)))
	(COND((NULL COMPI)(DSKIN COMPR)(ED T)(SETQ COMPI T)))
	(COMP LL)
AD002	(SETQ VN(THV ZN))
	(EVAL(LIST @DSKIN FILENAME))
	(COND((AND(NOT(NULL LL))(NOT(EQ @DSK:(CAR LL))))(RESTOREPROP)(REMPROP @RESTOREPROP @EXPR)))
	(THSETQ(THV ZN)(PLUS VN 10))
	(THSETQ(THV YN)(PLUS VN 10))
	(THSETQ(THV XN)(PLUS VN 10))
	(GO AD01)
AD2	(SETQ NA(READ))
	(COND((GET NA @THEOREM)(THVAL(LIST @THERASE NA)THALIST))
	     ((EQ @#(CAR(EXPLODE NA)))(DELAD NA)(GO AD01))
	     ((EQ NEGSGN(CAR(EXPLODE NA)))
	      (COND((GET(READLIST(CDR(EXPLODE NA)))@PARTIAL)(SETQ NA(READLIST(APPEND @(N)(CDR(EXPLODE NA)))))
		    (COND((GET(READLIST(CDR(EXPLODE NA)))@FLUENT)
			  (SETQ NA(CONS NA(APPEND(READ)@(R)))))
			 (T(SETQ NA(CONS NA(READ)))))
		    (COND((THVAL @(THGOAL(THEV NA))THALIST)(THVAL @(THERASE(THEV NA))THALIST))))
		   (T(SETQ NA(READLIST(CDR(EXPLODE NA))))
		     (COND((GET NA @FLUENT)(SETQ NA(CONS NA(APPEND(READ)@(R)))))
			  (T(SETQ NA(CONS NA(READ)))))
		     (COND((THVAL @(THNOT(THGOAL(THEV NA)))THALIST)(THVAL @(THASSERT(THEV NA))THALIST))))))
	     (T(COND((GET NA @FLUENT)(SETQ NA(CONS NA(APPEND(READ)@(R)))))
		    (T(SETQ NA(CONS NA(READ)))))
	       (COND((THVAL @(THGOAL(THEV NA))THALIST)(THVAL @(THERASE(THEV NA))THALIST))))  )

	(SETQ AL(CONS(REVERSE(CONS NA ADV))AL))
	(GO AD01)
AD3	(SETQ NA(READ))
	(COND((NOT(OR(GET NA @DEF)(AND(EQ NEGSGN(CAR(EXPLODE NA)))(GET(READLIST(CDR(EXPLODE NA)))@DEF))))
	      (SETQ AL(CONS(REVERSE(CONS NA ADV))AL))(GO AD02)))
	(COND((EQ NEGSGN(CAR(EXPLODE NA)))
	      (COND((GET(READLIST(CDR(EXPLODE NA)))@PARTIAL)(SETQ NA(READLIST(APPEND @(N)(CDR(EXPLODE NA)))))
		    (COND((GET(READLIST(CDR(EXPLODE NA)))@FLUENT)
			  (SETQ NA(CONS NA(APPEND(READ)@(R)))))
			 (T(SETQ NA(CONS NA(READ)))))
		    (COND((THVAL @(THNOT(THGOAL(THEV NA)))THALIST)(THVAL @(THASSERT(THEV NA))THALIST))))
		   (T(SETQ NA(READLIST(CDR(EXPLODE NA))))
		     (COND((GET NA @FLUENT)(SETQ NA(CONS NA(APPEND(READ)@(R)))))
			  (T(SETQ NA(CONS NA(READ)))))
		     (COND((THVAL @(THGOAL(THEV NA))THALIST)(THVAL @(THERASE(THEV NA))THALIST))))))
	     (T(COND((GET NA @FLUENT)(SETQ NA(CONS NA(APPEND(READ)@(R)))))
		    (T(SETQ NA(CONS NA(READ)))))
	       (COND((THVAL @(THNOT(THGOAL(THEV NA)))THALIST)(THVAL @(THASSERT(THEV NA))THALIST))))  )
	(SETQ AL(CONS(REVERSE(CONS NA ADV))AL))
	(GO AD01)
AD4	(SETQ NA(READ))
	(COND((NOT(GET NA @THEOREM))(PRINT NA)(PRINC @_IS_NOT_DEFINED)
	      (SETQ AN(SUB1 AN))(GO AD01)))
	(SETQ AL(CONS(REVERSE(CONS(GET NA @THEOREM)(CONS NA ADV)))AL))
	(THVAL @(THERASE(THEV NA))THALIST)
	(REMPROP NA @THEOREM)
	(GO AD02)
AD5	(SETQ NA(READ))
	(COND((NOT(OR(GET NA @DEF)(AND(EQ NEGSGN(CAR(EXPLODE NA)))(GET(READLIST(CDR(EXPLODE NA)))@DEF))))
	      (SETQ AL(CONS(REVERSE(CONS NA ADV))AL))(GO AD02)))
	(COND((EQ NEGSGN(CAR(EXPLODE NA)))
	      (COND((GET(READLIST(CDR(EXPLODE NA)))@PARTIAL)(SETQ NA(READLIST(APPEND @(N)(CDR(EXPLODE NA)))))
		    (COND((GET(READLIST(CDR(EXPLODE NA)))@FLUENT)
			  (SETQ NA(CONS NA(APPEND(READ)@(R)))))
			 (T(SETQ NA(CONS NA(READ)))))  )
		   (T(SETQ NA(READLIST(CDR(EXPLODE NA))))
		     (COND((GET NA @FLUENT)(SETQ NA(CONS NA(APPEND(READ)@(R)))))
			  (T(SETQ NA(CONS NA(READ)))))
		     (COND((THVAL @(THGOAL(THEV NA))THALIST)(THVAL @(THERASE(THEV NA))THALIST))))))
	     (T(COND((GET NA @FLUENT)(SETQ NA(CONS NA(APPEND(READ)@(R)))))
		    (T(SETQ NA(CONS NA(READ))))) ) )
	(SETQ OPT(READLIST(APPEND @(T)(EXPLODE(CAR NA)))))
	(PUTPROP OPT(LIST @THCONSE(PTHV(CDR NA))(CONS(CAR NA)(CDR NA))
			  (LIST @THSETQ @(THV ASSL)(LIST @CONS NA @(THV ASSL))))
		    @THEOREM)
	(THASSERT(THEV OPT))
	(SETQ AL(CONS(REVERSE(CONS OPT ADV))AL))
	(GO AD01)
AD6	(SETQ ADV(CONS(READ)ADV))
	(SETQ NA(CAR ADV))
	(COND((NOT(GET NA @THEOREM))(PRINT NA)(PRINC @_IS_NOT_DEFINED)(SETQ AN(SUB1 AN))(GO AD01)))
	(SETQ OPT(READ))
	(SETQ ADV(CONS OPT ADV))
	(SETQ ADV(CONS(READ)ADV))
	(COND((EQ OPT @TO)(SET(READLIST(APPEND @(R T)(EXPLODE NA)))
			      (APPEND(CAR ADV)(EVAL(READLIST(APPEND @(R T)(EXPLODE NA)))))))
	     ((EQ OPT @FROM)(SET(READLIST(APPEND @(R F)(EXPLODE NA)))
			        (APPEND(CAR ADV)(EVAL(READLIST(APPEND @(R F)(EXPLODE NA)))))))
	     (T(PRINT OPT)(PRINC @_IS_NOT_A_VALID_OPTION)(SETQ AN(SUB1 AN))(GO AD01)))
	(SETQ AL(CONS(REVERSE ADV)AL))
	(GO AD01)
AD7	(SETQ AN(SUB1 AN))
	(TERPRI)(TERPRI)
	(COND((NULL AL)(PRINT @NO_ADVICE_GIVEN_THIS_SESSION)(GO AD01)))
	(PRINT @**_ADVICE_GIVEN_DURING_THIS_SESSION_**)
	(TERPRI)
	(SETQ ALR(REVERSE AL))
AD03	(COND((NULL ALR)(GO AD01)))
	(COND((EQ @ALTER(CADAR ALR))(GO AD05)))
	(PRINT(CAR ALR))
	(SETQ ALR(CDR ALR))   (GO AD03)
AD05	(PRINT(LIST(CAAR ALR)(CADAR ALR)(CADDAR ALR)))
	(PRINT @DO_YOU_WANT_TO_SEE_PREVIOUS_VERSION?*)
	(COND((READ)(SPRINT(CADR(CDDAR ALR))2 2)))
	(PRINT @DO_YOU_WANT_TO_SEE_THE_PRESENT_VERSION?*)
	(COND((READ)(SPRINT(GET(CADDAR ALR)@THEOREM)2 2)))
	(SETQ ALR(CDR ALR))
	(GO AD03) 
AD8	(SETQ AN(SUB1 AN))
	(TERPRI)(TERPRI)
	(PRINT @RULES_ENTERED_AND_GOALS_PENDING_IN_CURRENT_SUBGOAL_TREE_PATH:)
	(PRINT @___)(PRTRULES CT ) 
	(TERPRI)
	(PRINT @CURRENT_PLAN:)
	(TSLPLAN(REVERSE(EVAL(CAR(THV ANS)))))
	(TERPRI)
	(PRINT @RULES_AND_GOALS_IN_LONGEST_PATH_OBTAINED_THUS_FAR:)
	(PRINT @___)(PRTRULES LCT) 
	(TERPRI)
	(PRINT @LONGEST_PLAN:)
	(TSLPLAN LGANS)
	(TERPRI)
	(GO AD01)  ))
EXPR)







(DEFPROP PRTRULES
   (LAMBDA(X)
      (PROG(TEM)
	(COND((NULL X)(RETURN NIL)))
	(SETQ TEM(REVERSE X))
PRT2	(PRINC(CAAR TEM))
	(SETQ TEM(CDR TEM))
	(COND(TEM(GO PRT2))) ))
EXPR)


(DEFPROP PTHV
   (LAMBDA(ARL)
	(COND((NULL ARL)NIL)
	     ((ATOM(CAR ARL))(PTHV(CDR ARL)))
	     (T(APPEND(LIST(CADAR ARL))(PTHV(CDR ARL))))))
EXPR)



(DEFPROP TREEPATH
   (LAMBDA(OP)
      (PROG NIL
	(SETQ CT (CONS(LIST(CAR OP))CT ))
	(THSETQ (THV CGL)(THVARSUBST(CADR OP)))
	(COND((*GREAT(LENGTH CT )(LENGTH LCT))
	      (SETQ LCT CT )))
	(RETURN T)))
FEXPR)


(DEFPROP TRACEINFO1
   (LAMBDA NIL
      (PROG NIL
	(PRINT @RULES_ENTERED_AND_GOALS_PENDING_IN_CURRENT_SUBGOAL_TREE_PATH:)
	(PRINT @___)
	(PRTRULES CT )       
	(TERPRI)
	(RETURN T) ))
EXPR)



(DEFPROP TRACEINFO2
   (LAMBDA (OP)
      (PROG NIL
	(PRINT(CAR OP))(PRINC @_IS_FAILING!!!!)
	(COND((NOT(ATOM(CAAR CT )))
	      (PRINT @___)(PRINC(CADAAR CT ))
	      (PRINC @_WAS_THE_LOSER) ))
	(TERPRI)
	(COND((AND(TTYIN)(ADVICESYS))(RETURN T)))
	(SETQ CT(CDR CT))
	(RETURN NIL) ))
FEXPR)



(DEFPROP DELAD1
   (LAMBDA(NU L)
	(COND((NULL L)NIL)
	     ((EQ NU(CAAR L))(DELAD1 NU(CDR L)))
	     (T(CONS(CAR L)(DELAD1 NU(CDR L))))))
EXPR)


(DEFPROP DELRL
   (LAMBDA(RL EL)
(PROG NIL (PRINT RL)(PRINT EL)
	(COND((NULL RL)NIL)
	     ((MEMQ(CAR RL)EL)(DELRL(CDR RL)EL))
	     (T(CONS(CAR RL)(DELRL(CDR RL)EL)))))
)
EXPR)


(DEFPROP DELAD
   (LAMBDA(NUM)
      (PROG(AD TE)
(PRINT @L1825)(PRINT NUM)
	(SETQ AN(SUB1 AN))
	(SETQ AD(ASSOC(READLIST(CDR(EXPLODE NUM)))AL))
	(COND((NULL AD)(PRINT @NO_SUCH_ADVICE_GIVEN)(RETURN T)))
	(SETQ AL(DELAD1(READLIST(CDR(EXPLODE NUM)))AL))
(PRINT @L1841)(PRINT AD)(PRINT AL)
	(SETQ AD(CDR AD))
	(GO(CDR(ASSOC(CAR AD)@((FOR . DE1)(DELETE . DE2)(ADD . DE3)(ALTER . DE4)(ASSUME . DE5)(RESTRICT . DE6)))))
DE1	(SETQ AD(CDR AD))
	(COND((EQ @FIRST(CADR AD))
	      (RPLACD(FBODY(GET(CAR AD)@THEOREM))
		     (CDDR(FBODY(GET(CAR AD)@THEOREM)))))
	     (T(RPLACD(FBODY(GET(CAR AD)@THEOREM))
		      (CDADDR(FBODY(GET(CAR AD)@THEOREM))))))
	(RETURN T)
DE2	(THVAL @(THASSERT(THEV(CADR AD)))THALIST)
	(RETURN T)
DE3	(THVAL @(THERASE(THEV(CADR AD)))THALIST)
	(RETURN T)
DE4	(THVAL @(THERASE(THEV(CADR AD)))THALIST)
	(REMPROP(CADR AD)@THEOREM)
	(PUTPROP(CADR AD)(CADDR AD)@THEOREM)
	(THVAL @(THASSERT(THEV(CADR AD)))THALIST)
	(RETURN T)
DE5	(THVAL @(THERASE(THEV(CADR AD)))THALIST)
	(RETURN T)
DE6	(SETQ TE(COND((EQ(CADDR AD)@TO)(READLIST(APPEND @(R T)(EXPLODE(CADR AD)))))
		     (T(READLIST(APPEND @(R F)(EXPLODE(CADR AD)))))))
	(SET TE(DELRL(EVAL TE)(CADDDR AD)))
	(RETURN T)   ))
EXPR)



(DEFPROP FILTERAX
   (LAMBDA(THM)
	(GET THM @AX)  )
EXPR)

(DEFPROP FILTEROP
   (LAMBDA(THM)
	(AND  
	   (OR(NOT(GET(CAAAR CT )@AX))(GET THM @AX))
	   (OR(GET(CAAAR CT )@REC)(NOT(EQ(CAAAR CT )THM)))
	   (OR(NULL(EVAL(READLIST(APPEND @(R T)(EXPLODE(CAAAR CT ))))))
	      (MEMQ THM(EVAL(READLIST(APPEND @(R T)(EXPLODE(CAAAR CT )))))))
	   (OR(NULL(EVAL(READLIST(APPEND @(R F)(EXPLODE(CAAAR CT ))))))
	      (NOT(MEMQ THM(EVAL(READLIST(APPEND @(R F)(EXPLODE(CAAAR CT ))))))))  ) )
EXPR)




(DEFPROP FBODY
   (LAMBDA(B)
	(COND((OR(EQ(CAAR(CDDDR B))@THGOAL)(AND(EQ(CAAR(CDDDR B))@THOR)
						(EQ(CAADAR(CDDDR B))@THAND)))
	      (CDDR B))
	     (T(FBODY(CDR B))))   )
EXPR)



(DEFPROP OPTIM
   (LAMBDA(PLN)
      (PROG(OPLN SUL)
	(SETQ OPLN(OPDEAD PLN PLN))
	

OP3	(COND((NULL SUL)(RETURN OPLN)))				
	(SETQ OPLN(SUBST(CAAR SUL)(CDAR SUL)OPLN))
	(SETQ GOL(SUBST(CAAR SUL)(CDAR SUL)GOL))
	(SETQ SUL(CDR SUL))
	(GO OP3)      ))
EXPR)


(DEFPROP OPDEAD
   (LAMBDA(PLNA PLN)
	(COND((ATOM PLNA)PLNA)
	     ((AND(EQ @←(CAR PLNA))(NOT(XRH(CADR PLNA)PLN))(NOT(XNA(CADR PLNA)PLN))
		  (COND((ATOM(CADDR PLNA))(SETQ SUL(CONS(CONS(CADDR PLNA)(CADR PLNA))SUL)))
		       (T T))   )
	      NIL)
	     (T(APPEND(CLIST(OPDEAD(CAR PLNA)PLN))(OPDEAD(CDR PLNA)PLN))))  )
EXPR)


(DEFPROP CLIST
   (LAMBDA(X)
	(COND((NULL X)NIL)
	     (T(LIST X))))
EXPR)


(DEFPROP XRH
   (LAMBDA(X P)
	(COND((ATOM P)NIL)
	     ((EQ @←(CAR P))(SUBSTP(CADDR P)X))
	     (T(OR(XRH X(CAR P))(XRH X(CDR P))))))
EXPR)


(DEFPROP XNA
   (LAMBDA(X P)
	(COND((EQ X P)T)
	     ((ATOM P)NIL)
	     ((EQ @←(CAR P))NIL)
	     (T(OR(XNA X(CAR P))(XNA X(CDR P))))))
EXPR)

(DEFPROP TSLPLAN
   (LAMBDA(P)
      (PROG(PL SEMCOL)
	(SETQ PL P)
	(COND((NULL PL)(RETURN NIL)))
	(SETQ INDENT(CONS @"   " INDENT))
	(TERPRI)
	(PRINDENT INDENT)
	(PRINC @BEGIN)(TERPRI)
T1	(PRINDENT INDENT)
	(TSLPLANI(CAR PL))
	(SETQ PL(CDR PL))
	(COND((NOT(NULL PL))(GO T1)))
	(PRINDENT INDENT)
	(PRINC @END)(TERPRI)
	(SETQ INDENT(CDR INDENT))
	(RETURN T)  )) 
EXPR)


(DEFPROP TSLPLANI
   (LAMBDA(PI)
      (PROG(PIT)
	(SETQ PIT PI)
	(COND((EQ(CAR PIT)@IF)(GO TS3))
	     ((EQ(CAR PIT)@WHILE)(GO TS6))
	     ((EQ(CAR PIT)@←)(GO TS9)) )
	(PF(LIST PIT))
	(COND((NULL(CDR PIT))(PRINC @;)(TERPRI)(RETURN T)))
	(GO TS13)
TS3	(SETQ PIT(CDR PIT))
	(PRINC @"IF ")
	(TSTCOND(CAR PIT))
	(SETQ PIT(CDR PIT))
	(PRINC @" THEN ")
	(SETQ PIT(CDR PIT))
	(COND((CDR PIT)(SETQ SEMCOL T)))
	(SETQ INDENT(CONS @"   " INDENT))
	(TERPRI)   (PRINDENT INDENT)
	(TSLPLANI(CAR PIT))
	(SETQ PIT(CDR PIT))
	(SETQ INDENT(CDR INDENT))
	(COND((NULL PIT)(RETURN T)))
	(SETQ PIT(CDR PIT))
(COND((NULL(CAR PIT))(GO TS13)))
	(PRINDENT INDENT)
	(PRINC @"ELSE ")
	(COND((AND(ATOM(CAAR PIT))(NOT SEMCOL))(TSLPLANI(CAR PIT))(GO TS13))
	     ((ATOM(CAAR PIT))(TSLPLANI(CAR PIT))(RETURN T))
	     (T(TSLPLAN(CAR PIT))(RETURN T)))
TS6	(SETQ PIT(CDR PIT))
	(PRINC @"WHILE ")
	(TSTCOND(CAR PIT))
	(SETQ PIT(CDDR PIT))
	(PRINC @" DO ")
	(TSLPLAN(CAR PIT))
	(RETURN T)
TS9	(SETQ PIT(CDR PIT))
	(PRINC(CAR PIT))
	(PRINC @" ← ")
	(SETQ PIT(CDR PIT))
	(COND((ATOM(CAR PIT))(GO TS11)))
	(COND((NOT(FUNDEF(CAR PIT)T))(GO TS13)))
(PF PIT)
	(GO TS13)
TS11	(PRINC(CAR PIT))
TS13	(COND((NOT SEMCOL)(PRINC @;))) (TERPRI)
	(RETURN T) ))
EXPR)


(DEFPROP FUNDEF
   (LAMBDA(FU SW)
      (PROG(FFL FAL AAL EAAL)
	(SETQ FFL(ASSOC(CAR FU)FUNDEFLIST))
	(COND((NULL FFL)(RETURN FU)))
	(SETQ FAL(CADR FFL))
	(SETQ FFL(CADDR FFL))
	(SETQ AAL(CDR FU))
FU3	(COND((ATOM(CAR AAL))(SETQ EAAL(CAR AAL)))
	     (T(SETQ EAAL(FUNDEF(CAR AAL)NIL))))
	(SETQ FFL(SUBST EAAL (CAR FAL)FFL))
	(SETQ AAL(CDR AAL))
	(SETQ FAL(CDR FAL))
	(COND(FAL(GO FU3)))
	(COND(SW(MAPC(FUNCTION NPRINC)FFL))
	     (T(RETURN FFL)))
	(RETURN NIL)  ))
EXPR)



(DEFPROP NPRINC
   (LAMBDA(FF)
	(COND((ATOM FF)(PRINC FF))
	     (T(MAPC(FUNCTION NPRINC)FF)))  )
EXPR)


(DEFPROP PRINDENT
   (LAMBDA(I)
      (PROG(II)
	(SETQ II I)
PR4	(PRINC(CAR II))
	(SETQ II(CDR II))
	(COND((NULL II)(RETURN T))
	     (T(GO PR4)))  ))
EXPR)


(DEFPROP TSTCOND
   (LAMBDA(C)
      (PROG(CC CC1)
	(SETQ CC C)
TS0     (COND((ATOM(CAR C))(SETQ CC1 CC))
             (T(SETQ CC1(CAR CC))))
	(COND((NOT(EQ NEGSGN(CAR CC1)))(GO TS2)))
	(PRINC NEGSGN)
	(SETQ CC1(CDR CC1))
TS2	(PF(LIST CC1))
        (SETQ CC(CDR CC))
        (COND((OR(ATOM(CAR C))(NULL CC))(RETURN T)))
        (PRINC @"  ")(PRINC @∧)(PRINC @"  ")
        (GO TS0)  ))
EXPR)

(DEFPROP UNCERTLIT
   (LAMBDA(LI DSW LI1 LI2)
      (PROG NIL
	(SETQ UNCERTLIST(APPEND UNCERTLIST(LIST LI)))
	(RPLACA CT(CONS(CAAR CT)(UPDATLIT(CDAR CT)LI1 @X)))
	(RPLACA CT(CONS(CAAR CT)(UPDATLIT(CDAR CT)LI2 @X)))
	(COND(DSW(RETURN NIL))
	     (T(RETURN T)))  ))
EXPR)

(DEFPROP FINDINSTANG
   (LAMBDA(CTH)
	(COND((NULL CTH)NIL)
	     ((NULL(CDR CTH))(RPLACA CTH(CONS(CAAR CTH)(CONS @IF(CDAR CTH))))GOL)
	     ((NOT(SUBSTP(CAR(CDAADR CTH))@THV))
	      (RPLACA CTH(CONS(CAAR CTH)(CONS @IF(CDAR CTH))))
	      (CAR(CDAADR CTH)))
	     (T(FINDINSTANG(CDR CTH))))   )
EXPR)

(DEFPROP CONDSTAT
   (LAMBDA(G DSW)
      (PROG (TE GL PRLIST)
	(COND((AND(NULL UNCERTLIST)DSW)(RETURN NIL))
	     ((NULL UNCERTLIST)(RETURN T)))
	(COND((NOT(SUBSTP G @THV))(SETQ GL G)(RPLACA CT(CONS(CAAR CT)(CONS @IF(CDAR CT)))))
	     (T(SETQ GL(FINDINSTANG CT))))
	(SETQ SSW T)
         (SETQ TE(CONS(APPEND(LIST @IF(TSTLIT2(CAR UNCERTLIST)) @THEN)
			    (LIST(NESTIF(LIST(CAR UNCERTLIST))(CDR UNCERTLIST)GL))@(ELSE))(EVAL(CAR(THV ANS)))))
	(THSET(CAR(THV ANS))TE)
	(THASSERT(THEV(CAR UNCERTLIST)))
	(THSETQ(THV PASSUM)(CONS(CAR UNCERTLIST)(THV PASSUM)))
	(SETQ UNCERTLIST NIL)
	(THSETQ(THV PROCLIST)(CONS PRLIST(THV PROCLIST)))
	(THSETQ(THV ANS)(CONS(LIST @THV(GENSYM))(THV ANS)))
	(THVSET(CAR(THV ANS))NIL)
	(SETQ SSW NIL)
	(RETURN T)  ))
EXPR)


(DEFPROP NESTIF
   (LAMBDA(FL TL GL)
	(COND((NULL TL)(PROCALL FL TL GL))
             (T(APPEND(LIST @IF(TSTLIT2(CAR TL))@THEN)
		      (LIST(NESTIF(CONS(CAR TL)FL)(CDR TL)GL))
		      (LIST @ELSE (PROCALL FL TL GL))))))
EXPR)


(DEFPROP PROCALL
   (LAMBDA(FL TL GL)
      (PROG(PL ST PFL LI QFL)
	(SETQ PFL FL)
	(SETQ PL(READLIST(APPEND @(P R O C)(EXPLODE(SETQ PN(ADD1 PN))))))
	(SETQ PRLIST(CONS PL PRLIST))
	(SETQ ST(CONS(READLIST(APPEND @(S T A T)(EXPLODE(SETQ SN(ADD1 SN)))))@CST))
	(COND(TL(THVAL @(THASSERT(THEV(CAR TL)))THALIST)))
PR2	(SETQ LI(CAR PFL))
	(COND((EQ @N(CAR(EXPLODE(CAR LI))))
	      (SETQ LI(CONS(READLIST(CDR(EXPLODE(CAR LI))))(CDR LI))))
	     (T(SETQ LI(CONS(READLIST(CONS @N(EXPLODE(CAR LI))))(CDR LI)))))
	(SETQ QFL(CONS LI QFL))
	(THASSERT(THEV LI))
	(SETQ PFL(CDR PFL))
	(COND(PFL(GO PR2)))
	(EVAL(LIST @OUTC(LIST @OUTPUT @DSK: ST)T))
	(THDUMP)
	(OUTC NIL)
PR4	(THERASE(THEV(CAR QFL)))
	(SETQ QFL(CDR QFL))
	(COND(QFL(GO PR4)))
	(COND(TL(THVAL @(THERASE(THEV(CAR TL)))THALIST)))
	(SETQ FIFOL(APPEND FIFOL(LIST(LIST PL GL ST))))
        (THSETQ(THV COMMENTLIST)(CONS(LIST  PL @ATTEMPTS_TO_ACHIEVE_
					   (TSTLIT GL))(THV COMMENTLIST)))
	(RETURN(APPEND(LIST PL)(CDR(TSTLIT GL))))  ))
EXPR)

(DEFPROP INSTANTHV
   (LAMBDA(LL)
	(COND((NULL LL)NIL)
	     ((ATOM LL)LL)
	     ((EQ(CAR LL)@THV)(THVAL LL THALIST))
	     (T(CONS(INSTANTHV(CAR LL))(INSTANTHV(CDR LL))))))
EXPR)


(DEFPROP DISPOST
   (LAMBDA(DNF)
      (PROG(TE PRLIST)
	(SETQ SSW T)
	(SETQ DNF(INSTANTHV DNF))
	(SETQ TE(CONS(APPEND(LIST @IF(NRTSTLITS(PTESTLITS(CADR DNF)(APPEND(CDDR DNF)(LIST(CAR DNF)))))@THEN)
			    (LIST(NESTIFP(LIST(CAR DNF))(CDR DNF)(CAAR DNF))))
		     (EVAL(CAR(THV ANS)))))
	(THSET(CAR(THV ANS))TE)
	(THSETQ(THV PROCDATA)(CONS(LIST PRLIST(THV DBLITS)(THV ASSERTLITS))
				  (THV PROCDATA)))
	(SETQ SSW NIL)
	(RETURN T)   ))
EXPR)


(DEFPROP NESTIFP
   (LAMBDA(ADF DF GLP)
	(COND((NULL(CDR  DF))(PROCALLP(APPEND DF ADF) GLP))
	     (T(APPEND(LIST @IF(NRTSTLITS(PTESTLITS(CADR DF)(APPEND(CDDR DF)(CONS(CAR DF)ADF))))@THEN)
		      (LIST(NESTIFP(CONS(CAR DF)ADF)(CDR DF)GLP))
		      (LIST @ELSE(PROCALLP (APPEND DF ADF) GLP)))))   )
EXPR)


(DEFPROP TSTLIT
   (LAMBDA(LI)
	(COND((EQ @R(CAR(LAST LI)))(REVERSE(CDR(REVERSE LI))))
	     (T LI))   )
EXPR)


(DEFPROP PROCALLP
   (LAMBDA(DF GLP)
      (PROG(PL ST CL SSW CLL)
         (SETQ CLL DF)
	(SETQ PL(READLIST(APPEND @(P R O C)(EXPLODE(SETQ PN(ADD1 PN))))))
	(SETQ PRLIST(CONS PL PRLIST))
	(SETQ ST(CONS(READLIST(APPEND @(S T A T)(EXPLODE(SETQ SN(ADD1 SN)))))@CST))
	(SAVESTATE @XXXX)
	(THFLUSH THASSERTION THERASING THCONSE)
	(DSKIN CURSTATE)
	(COND((NULL DF)(GO PR7)))
PR1      (SETQ CL(CAR CLL))
PR3      (ASSERTPOST(CAR CL)SSW)
         (SETQ CL(CDR CL))
         (COND(CL(GO PR3)))
         (SETQ SSW T)
         (SETQ CLL(CDR CLL))
         (COND(CLL(GO PR1)))
PR7	(EVAL(LIST @OUTC(LIST @OUTPUT @DSK: ST)T))
	(THDUMP)(OUTC NIL)
	(SETQ FIFOL(APPEND FIFOL(LIST(LIST PL GLP ST))))
	(THFLUSH THASSERTION THERASING THCONSE)
	(DSKIN XXXX)
	(THSETQ(THV COMMENTLIST)(CONS(LIST  PL @ATTEMPTS_TO_ACHIEVE_
					   (TSTLIT GLP))(THV COMMENTLIST)))
	(RETURN(APPEND(LIST PL)(CDR(TSTLIT GLP))))   ))
EXPR)


(DEFPROP SAVESTATE
   (LAMBDA(SS)
      (PROG  NIL
	(EVAL(LIST @OUTC(LIST @OUTPUT @DSK: SS)T))
	(THDUMP)
	(OUTC NIL)   (RETURN T)  ))
EXPR)

(DEFPROP TSTLIT2
   (LAMBDA(LI)
      (PROG(LIT)
(SETQ LIT LI)
        (COND((EQ @R(CAR(LAST LI)))
              (SETQ LIT(REVERSE(CDR(REVERSE LI))))))
        (COND((EQ NEGSGN(CAR LI))
              (SETQ LIT(CDR LIT)))
             ((EQ @N(CAR(EXPLODE(CAR LI))))
              (SETQ LIT(CONS(READLIST(CDR(EXPLODE(CAR LI))))(CDR  LIT))))
             (T(SETQ LIT(CONS NEGSGN LIT))))
        (RETURN LIT)  ))
EXPR)


(DEFPROP PTESTLITS
   (LAMBDA(PO NEG)
        (COND((NULL NEG)(LIST(TSTLIT(CAR PO))))
             (T(CONS(TSTLIT2(CAAR NEG))(PTESTLITS PO(CDR NEG))))))
EXPR)


(DEFPROP NRTSTLITS
   (LAMBDA(LL)
        (COND((MEMBER(CAR(LAST LL))(CDR(REVERSE LL)))
              (CDR(REVERSE LL)))
             (T(REVERSE LL))))
EXPR)


(DEFPROP ASSERTPOST
   (LAMBDA(LI SW)
      (PROG(NSW LIT PSW)
        (COND((EQ @N(CAR(EXPLODE(CAR LI))))
              (SETQ LIT(CONS(READLIST(CDR(EXPLODE(CAR LI))))(CDR  LI)))
              (SETQ NSW T))
             (T(SETQ LIT LI)))
        (COND((GET(CAR LIT)@PARTIAL)(SETQ PSW T)))
        (COND((OR(AND NSW PSW(NOT SW))
                 (AND(NOT NSW)PSW(NOT SW))
                 (AND(NOT NSW)(NOT PSW)(NOT SW))
                 (AND NSW(NOT PSW)SW))
              (THASSERT(THEV(CONS(READLIST(CONS @N(EXPLODE(CAR LI))))(CDR LI))))))
        (RETURN T)   ))
EXPR)




(DEFPROP ELSECLAUSE
   (LAMBDA NIL
      (PROG(CB IFS)
	(SETQ IFS(CDAR CT))
	(THSETQ CT(CDR CT)T T)
EL2	(SETQ CB(REVERSE(EVAL(CAR(THV ANS)))))
	(THSETQ(THV ANS)(CDR(THV ANS)))
	(THSET(CAR(THV ANS))(CONS(APPEND(CAR(EVAL(CAR(THV ANS))))
					(LIST CB))
				 (CDR(EVAL(CAR(THV ANS)))))  )
	(SETQ GANS(REVERSE(EVAL(CAR(THV ANS)))))
	(THSETQ(THV PROCDATA)(CONS(LIST(CAR(THV PROCLIST))(THV DBLITS)(THV ASSERTLITS))
				  (THV PROCDATA)))
	(THSETQ(THV PROCLIST)(CDR(THV PROCLIST))T T)
	(SETQ IFS(CDR IFS))
	(COND((NULL IFS)(RETURN T)) ((ATOM(CAR IFS))(GO EL2)))
	(RETURN T)   ))
EXPR)



(DEFPROP SUBPLANL
   (LAMBDA(P PL)
	(COND((NULL PL)P)
	     (T(SUBPLANL(SUBPLANL1 P(CAR PL))(CDR PL)))))
EXPR)


(DEFPROP SUBPLANL1
   (LAMBDA(P PL)
	(COND((ATOM P)P)
	     ((AND(NOT(ATOM(CAR P)))(EQ @←(CAAR P))(EQ(CAADDR(CAR   P))(CAAR PL)))
              (SUBPLANL1(APPEND(REVERSE(SUBPLANL2(CAR P)PL))(CDR P))PL))
	     (T(CONS(SUBPLANL1(CAR P)PL)(SUBPLANL1(CDR P)PL)))))
EXPR)


(DEFPROP SUBPLANL2
   (LAMBDA(P PL)
      (PROG(PT PLT BOD)
(PRINT @L36625)(PRINT P)(PRINT PL)
	(SETQ PT P)(SETQ PLT PL)
	(SETQ BOD(CADR PLT))
	(SETQ BOD(SUBST(CADR PT)(CADAR PLT)BOD))
	(SETQ PT(CDADDR PT))
	(SETQ PLT(CDDAR PLT))
SU2	(COND((NULL PT)(RETURN BOD)))
	(SETQ BOD(SUBST(CAR PT)(CAR PLT)BOD))
	(SETQ PT(CDR PT))
	(SETQ PLT(CDR PLT))
	(GO SU2)   ))
EXPR)

(DEFPROP DELL
   (LAMBDA(C L)
	(COND((NULL L)NIL)
	     ((AND(CDDR C)(CDDAR L)(EQUAL(CAR C)(CAAR L))
		  (EQUAL(CADR C)(CADAR L))
		  (COND((CADDR C)(EQUAL(CADDR C)(CADDAR L)))
		       (T T)))
	      (CDR L))
	     ((AND(NULL(CDDR C))(NULL(CDDAR L))(EQUAL(CAR C)(CAAR L))
		  (COND((CADR C)(EQUAL(CADR C)(CADAR L)))
		       (T T)))
	      (CDR L))
	     (T(CONS(CAR L)(DELL C(CDR L)))))  )
EXPR)


(DEFPROP FINDC
   (LAMBDA(C L)
	(COND((NULL L)NIL)
	     ((AND(CDDR C)(CDDAR L)(EQUAL(CAR C)(CAAR L))
		  (EQUAL(CADR C)(CADAR L))
		  (COND((CADDR C)(EQUAL(CADDR C)(CADDAR L)))
		       (T T)))
	      (CAR L))
	     ((AND(NULL(CDDR C))(NULL(CDDAR L))(EQUAL(CAR C)(CAAR L))
		  (COND((CADR C)(EQUAL(CADR C)(CADAR L1)))
		       (T T)))
	      (CAR L))
	     (T(FINDC C(CDR L))))  )
EXPR)

(DEFPROP ELEVA
   (LAMBDA(C L)
	(COND((NULL L)NIL)
	     ((AND(NULL(CDDAR L))(EQUAL(CAAR C)(CADAAR L)))
	      (SETQ SW T)(CONS(LIST(CAAR L)(NRCONJ(CADAR L)(CADR C)))
			      (CDR L)))
	     (T(CONS(CAR L)(ELEVA C(CDR L)))))  )
EXPR)


(DEFPROP ELEVB
   (LAMBDA(C L)
	(COND((NULL L)NIL)
	     ((AND(NULL(CDDAR L))(EQUAL(CADAR C)(CAAAR L)))
	      (SETQ SREL(NRCONJ(CADAR L)(CADR C)))
	      (CDR L))
	     (T(CONS(CAR L)(ELEVB C(CDR L)))))  )
EXPR)


(DEFPROP ELEVC
   (LAMBDA(C L)
	(COND((NULL L)NIL)
	     ((AND(NULL(CDDAR L))(EQUAL(CAR C)(CAAR L)))
	      (SETQ SREL(NRCONJ(CADAR L)(CADR C)))
	      (SETQ SW T)
	      (CDR L))
	     (T(CONS(CAR L)(ELEVC C(CDR L)))))  )
EXPR)


(DEFPROP NRCONJ
   (LAMBDA(R1 R2)
	(COND((NULL R2)R1)
	     ((MEMBER(CAR R2)R1)(NRCONJ R1(CDR R2)))
	     (T(CONS(CAR R2)(NRCONJ R1(CDR R2)))))  )
EXPR)


(DEFPROP WHILASSEM
   (LAMBDA(BP IP CL CT )
      (PROG(ALP ALS PA Y Z W R SASG SASGR TE ALF BET WFT ALFT RP)
(PRINT @L37410)(PRINT BP)(PRINT IP)(PRINT CL)(PRINT CT)
(PRINT @L37415)(PRINT(THV SASSERTLITS))(PRINT(THV ASSERTLITS))
	(SETQ WFT(THV FT))
(PRINT @L37425)(PRINT CL)(PRINT WFT)
	(SETQ IP(REVERSE IP))
WH2	(SETQ PA(CAR CL))
(PRINT @L37432)(PRINT PA)(PRINT WFT)
	(SETQ Y(READLIST(APPEND(LIST @Y)(EXPLODE(THSETQ(THV YN)(ADD1(THV YN)))))))
	(SETQ Z(READLIST(APPEND(LIST @Z)(EXPLODE(THSETQ(THV ZN)(ADD1(THV ZN)))))))
	(COND((CDDR PA)(SETQ ALF(CAR PA))(SETQ BET(CADR PA)))
	     (T(SETQ ALF(CAAR PA))(SETQ BET(CADAR PA))))
	(SETQ ALFT(COND((CDDAR WFT)(CAAR WFT))(T(CAAAR WFT))))
	(SETQ BP(CONS(LIST @← Y ALFT)BP))
	(SETQ LIFOL(CONS(COND((THASVAL(THV NT))(SUBST Y ALFT(SUBST Z ALF(CAR LIFOL) )))
		(T(SUBST Y ALFT(SUBST Z BET(CAR LIFOL)))))  (CDR LIFOL)))
	(SETQ IP(APPEND IP(LIST(LIST @← Y Z))))
	(SETQ ALP(CONS(CONS ALF Y)ALP))
	(SETQ ALS(CONS(CONS BET Z)ALS))
(PRINT @L37456)(PRINT PA)
	(COND((CDDR PA)(SETQ SASG(APPEND(LIST(LIST @← Z(CADDR PA)))
					     SASG))(GO WH4)))
	(SETQ R(CADR PA))
	(SETQ R(APPEND(LIST(CAR R))(COND((CDR R)(COND((CDDR R)(LIST  (CADR R)  (CADDR R)))
						     (T(LIST  (CADR R)))))
					(T NIL))))
	(SETQ W(READLIST(APPEND(LIST @W)(EXPLODE(THV ZN)))))
	(SETQ RP R)
	(SETQ R(SUBST W BET R))
	(COND((EQUAL R RP)(SETQ R(SUBST W ALF R))))
	(SETQ SASGR(APPEND (LIST(LIST @IF R @THEN(LIST @← Z W)))SASGR))
WH4	(SETQ CL(CDR CL))
	(SETQ WFT(CDR WFT))
	(COND(CL(GO WH2)))
(PRINT @L38525)(PRINT ALP)(PRINT ALS)(PRINT SASG)(PRINT SASGR)
	(SETQ ALP(DEQ ALP))
	(SETQ ALS(DEQ ALS))
	(SETQ SASG(REVERSE(VSUB ALP SASG)))
	(SETQ SASGR(REVERSE(VSUB ALP SASGR)))
	(SETQ IP(VSUB ALS IP))
	(SETQ IP(VSUB ALP IP))
	(SETQ CT(VSUB ALP CT))
	(SETQ TE(SUBPLANL(APPEND(LIST(LIST @WHILE(CONS NEGSGN  CT)@DO(APPEND SASG IP SASGR)))(APPEND SASGR BP))(THV PLANL)))
(PRINT TE)
	(RETURN TE) ))
EXPR)


(DEFPROP DEQ
   (LAMBDA(SAL)
	(COND((NULL SAL)NIL)
	     (T(CONS(CAR SAL)(DEQ(DEQ1(CAR SAL)(CDR SAL)))))))
EXPR)

(DEFPROP DEQ1
   (LAMBDA(A D)
	(COND((NULL D)NIL)
	     ((EQUAL(CAR A)(CAAR D))(DEQ1 A(CDR D)))
	     (T(CONS(CAR D)(DEQ1 A(CDR D))))))
EXPR)


(DEFPROP COMPCHANGES
   (LAMBDA(IN1 IN2 ACL)
      (PROG(CL1 L1 L2 UL UA A1 A2 LCL SREL SW CREL)
(PRINT @L38815)(PRINT ACL)(PRINT IN1)(PRINT IN2)
CO2	(SETQ L1(CAR IN1))   (SETQ L2(CAR IN2))
	(SETQ UL(ELASSOC L2 ACL))
	(SETQ LCL NIL) 
	(SETQ CREL(COND((EQ @R(CAR(REVERSE L1)))(REVERSE(CDR(REVERSE L1))))
		       (T L1)))
	(SETQ L1(CDR L1))   (SETQ L2(CDR L2))
	(COND((EQUAL L1 L2)(GO CO8)))
CO4	(SETQ A1(CAR L1))  (SETQ A2(CAR L2))   (SETQ SW NIL)
	(SETQ UA(COND(UL(CAR UL))(T NIL)))
(PRINT @L38834)(PRINT CL1)(PRINT LCL)(PRINT A1)(PRINT A2)(PRINT UA)
	(COND((EQUAL A1 A2)(GO CO6)))
	(COND((AND(NULL UA)(OR(NOT(EQUAL(SUBST @# A1 A2)A2))
			      (NOT(EQUAL(SUBST @# A2 A1)A1))))
	      (GO CO6)))
	(COND((AND UA(ATOM UA)(NOT(EQUAL(SUBST @# A1 A2)A2)))
	      (COND((AND(NOT(FINDC(LIST A1 A2 NIL)CL1))
		        (NOT(FINDC(LIST A1 A2 NIL)LCL)))
		    (SETQ LCL(CONS(LIST A1 A2 A2)LCL))
		    (GO CO6))
		   (T(GO CO6)))  ))
	(COND((AND UA(ATOM UA))(GO CO6)))
	(COND((AND(NOT(ATOM UA))(NOT(MEMBER(LIST A1 A2 UA)CL1))
		  (NOT(MEMBER(LIST A1 A2 UA)LCL)))
	      (SETQ CL1(DELL(LIST A1 A2 NIL)CL1))
	      (SETQ CL1(DELL(LIST(LIST A1 A2)NIL)CL1))
	      (SETQ LCL(DELL(LIST A1 A2 NIL)LCL))
	      (SETQ LCL(CONS(LIST A1 A2 UA)LCL))
	      (GO CO6)))
	(COND((AND(NULL UA)(OR(FINDC(LIST A1 A2 NIL)CL1)
			      (FINDC(LIST(LIST A1 A2)(LIST CREL))CL1)))
	      (GO CO6)))
	(COND((NULL UA)(SETQ SREL (LIST CREL)))
	     (T(GO CO6)))
	(SETQ CL1(ELEVA(LIST(LIST A1 A2)SREL)CL1))
	(COND(SW(GO CO6)))
	(SETQ LCL(ELEVA(LIST(LIST A1 A2)SREL)LCL))
	(COND(SW(GO CO6)))
	(SETQ CL1(ELEVB(LIST(LIST A1 A2)SREL)CL1))
	(SETQ LCL(ELEVB(LIST(LIST A1 A2)SREL)LCL))
	(SETQ CL1(ELEVC(LIST(LIST A1 A2)SREL)CL1))
	(SETQ LCL(ELEVC(LIST(LIST A1 A2)SREL)LCL))
	(COND(SW(SETQ LCL(CONS(LIST(LIST A1 A2)SREL)LCL))(GO CO6)))
	(SETQ LCL(CONS(LIST(LIST A1 A2)SREL)LCL))
CO6	(SETQ L1(CDR L1))    (SETQ L2(CDR L2))
	(COND(UL(SETQ UL(CDR UL))))
	(COND(L1(GO CO4)))
	(SETQ CL1(APPEND LCL CL1))
CO8	(SETQ IN1(CDR IN1))
	(SETQ IN2(CDR IN2))
	(COND(IN1(GO CO2)))
	(RETURN CL1)  ))
EXPR)
(DEFPROP REM#
   (LAMBDA(A)
	(COND((ATOM A)A)
	     ((EQ @#(CAR A))(CADDR A))
	     (T(CONS(REM#(CAR A))(REM#(CDR A))))))
EXPR)


(DEFPROP AMBIG
   (LAMBDA(CHL)
	(COND((NULL CHL)NIL)
	     ((AMBIG1(CAR CHL)(CDR CHL))T)
	     (T(AMBIG(CDR CHL))))  )
EXPR)

(DEFPROP AMBIG1
   (LAMBDA(AC DC)
	(COND((NULL DC)NIL)
	     ((AMBIG2(AMBIG3 AC)(AMBIG3(CAR DC)))T)
	     (T(AMBIG1 AC(CDR DC))))  )
EXPR)

(DEFPROP AMBIG2
   (LAMBDA(P1 P2)
	(OR(EQUAL(CAR P1)(CAR P2))  (EQUAL(CADR P1)(CADR P2))
	   (EQUAL(CAR P1)(CADR P2))(EQUAL(CADR P1)(CAR P2))    )  )
EXPR)

(DEFPROP AMBIG3
   (LAMBDA(C)
	(COND((CDDR C)(LIST(CAR C)(CADR C)))
	     (T(CAR C)))  )
EXPR)

(DEFPROP REMBT
   (LAMBDA(A)
      (PROG NIL
	(GO RE1)
	(THDO(PRED1ARG P1A))
	(THDO(PRED2ARG P2A))
	(THDO(PRED3ARG P3A))
	(THDO(PRED4ARG P4A))
	(THDO(PRED5ARG P5A))
RE1	(RETURN(REM# A))   ))
EXPR)


(DEFPROP PRED1ARG
   (LAMBDA(X)
      (THPROG(P)
	(THAMONG(THV P)X)
A	(THFIND ALL
		(THEV(THDO
		   (THERASE((THV P)(THV Y1)))
		   (THASSERT((THV P)(THEV(CADDR(THV Y1)))))  ))
		(Y1)
		(THGOAL((THV P)(THNV Y1)))
		(EQ @#(CAR(THV Y1)))  )
	(THFINALIZE THTAG A)
	(THFAIL)   ))
EXPR)


(DEFPROP PRED2ARG
   (LAMBDA(X)
      (THPROG(P)
	(THAMONG(THV P)X)
A	(THFIND ALL
		(THEV(THDO
		   (THERASE((THV P)(THV Y1)(THV Y2)))
		   (THASSERT((THV P)(THEV(CHECK#(THV Y1)))
				    (THEV(CHECK#(THV Y2))) ))  ))
		(Y1 Y2)
		(THGOAL((THV P)(THNV Y1)(THNV Y2)))
		(THOR(EQ @#(CAR(THV Y1)))(EQ @#(CAR(THV Y2)))) )
	(THFINALIZE THTAG A)
	(THFAIL)   ))
EXPR)


(DEFPROP PRED3ARG
   (LAMBDA(X)
      (THPROG(P)
	(THAMONG(THV P)X)
A	(THFIND ALL
		(THEV(THDO
		   (THERASE((THV P)(THV Y1)(THV Y2)(THV Y3)))
		   (THASSERT((THV P)(THEV(CHECK#(THV Y1)))
				    (THEV(CHECK#(THV Y2)))
				    (THEV(CHECK#(THV Y3))) ))  ))
		(Y1 Y2 Y3)
		(THGOAL((THV P)(THNV Y1)(THNV Y2)(THNV Y3)))
		(THOR(EQ @#(CAR(THV Y1)))(EQ @#(CAR(THV Y2)))(EQ @#(CAR(THV Y3)))) )
	(THFINALIZE THTAG A)
	(THFAIL)   ))
EXPR)


(DEFPROP PRED4ARG
   (LAMBDA(X)
      (THPROG(P)
	(THAMONG(THV P)X)
A	(THFIND ALL
		(THEV(THDO
		   (THERASE((THV P)(THV Y1)(THV Y2)(THV Y3)(THV Y4)))
		   (THASSERT((THV P)(THEV(CHECK#(THV Y1)))
				    (THEV(CHECK#(THV Y2)))
				    (THEV(CHECK#(THV Y3)))
				    (THEV(CHECK#(THV Y4))) ))  ))
		(Y1 Y2 Y3 Y4)
		(THGOAL((THV P)(THNV Y1)(THNV Y2)(THNV Y3)(THNV Y4)))
		(THOR(EQ @#(CAR(THV Y1)))(EQ @#(CAR(THV Y2)))(EQ @#(CAR(THV Y3)))(EQ @#(CAR(THV Y4)))) )
	(THFINALIZE THTAG A)
	(THFAIL)   ))
EXPR)


(DEFPROP PRED5ARG
   (LAMBDA(X)
      (THPROG(P)
	(THAMONG(THV P)X)
A	(THFIND ALL
		(THEV(THDO
		   (THERASE((THV P)(THV Y1)(THV Y2)(THV Y3)(THV Y4)(THV Y5)))
		   (THASSERT((THV P)(THEV(CHECK#(THV Y1)))
				    (THEV(CHECK#(THV Y2)))
				    (THEV(CHECK#(THV Y3)))
				    (THEV(CHECK#(THV Y4)))
				    (THEV(CHECK#(THV Y5))) ))  ))
		(Y1 Y2 Y3 Y4 Y5)
		(THGOAL((THV P)(THNV Y1)(THNV Y2)(THNV Y3)(THNV Y4)(THNV Y5)))
		(THOR(EQ @#(CAR(THV Y1)))(EQ @#(CAR(THV Y2)))(EQ @#(CAR(THV Y3)))(EQ @#(CAR(THV Y4)))(EQ @#(CAR(THV Y5)))) )
	(THFINALIZE THTAG A)
	(THFAIL)   ))
EXPR)



(DEFPROP TRSUBSTP
   (LAMBDA(PL ELT)
	NIL)
EXPR)



(DEFPROP TRSUBST
   (LAMBDA(NE OE PL)
	(SUBST NE OE PL))
EXPR)



(DEFPROP SUBSTP
   (LAMBDA(P V)
	(COND((EQUAL P V)T)
	     ((ATOM P)NIL)
	     (T(OR(SUBSTP(CAR P)V)(SUBSTP(CDR P)V)))))
EXPR)




(DEFPROP VSUB
   (LAMBDA(RL PL)
      (PROG(CRL SPL DONE CRL1)
	(COND((NULL PL)(RETURN NIL)))
	(SETQ CRL RL)
	(SETQ SPL PL)
VS1	(COND(DONE(GO VS3)))
	(SETQ DONE T)
	(SETQ CRL(RECSUB1 CRL CRL))
	(GO VS1)
VS3	(COND((NOT DONE)(RETURN SPL)))
	(SETQ CRL1 CRL)
	(SETQ DONE NIL)
VS5	(COND((NULL CRL1)(GO VS3)))
	(COND((OR(SUBSTP SPL(CAAR CRL1))(TRSUBSTP SPL(CAAR CRL1)))(SETQ DONE T)))
	(SETQ SPL(TRSUBST(CDAR CRL1)(CAAR CRL1)SPL))
	(SETQ CRL1(CDR CRL1))
	(GO VS5)    ))
EXPR)


(DEFPROP RECSUB1
   (LAMBDA(RL1 RL2)
	(COND((NULL RL1)RL2)
	     (T(RECSUB1(CDR RL1)(APPEND(RECSUB2(CAR RL1)RL2)RL2))))  )
EXPR)


(DEFPROP RECSUB2
   (LAMBDA(RL11 RL22)
	(COND((NULL RL22)NIL)
	     ((AND(OR(SUBSTP(CAAR RL22)(CAR RL11))(TRSUBSTP(CAAR RL22)(CAR RL11)))(NOT(EQ(CDR RL11)(CDAR RL22))))
	      ((LAMBDA(S)(COND((MEMBER S RL2)(RECSUB2 RL11(CDR RL22)))
			      (T(APPEND(SETQ DONE NIL)(LIST S)
				       (RECSUB2 RL11(CDR RL22))))))
			 (TRSUBST(CDR RL11)(CAR RL11)(CAR RL22))))
	     (T(RECSUB2 RL11(CDR RL22))))  )
EXPR)


(OPS (TDNE 612000)(TTCALL 51000))
(LAP TTYIN SUBR)
(TTCALL 2 1)
(CLEARM 0 1)
(TDNE 1 '(C 777777 0 777760))
(POPJ P 0)
(CLEARM 0 1)
(POPJ P 0)
NIL


(DEFPROP CJOINCOND
   (LAMBDA NIL
      (PROG(PD LDB LA)
JO3	(SETQ LDB(CADAR(THV PROCDATA)))
	(SETQ LA(CADDAR(THV PROCDATA)))
	(COND((EQUAL(LENGTH LDB)(LENGTH(THV DBLITS)))(PRINT @YES)(GO JO6)))
	(SETQ LDB(REVERSE(INCRELIT LDB(REVERSE(THV DBLITS)))))
	(SETQ LA(REVERSE(INCRELIT LA(REVERSE(THV ASSERTLITS)))))
	(SETQ LDB(DBREF LDB LA))
	(SETQ JOINCOND(CONS(LIST(CAAR(THV PROCDATA))LDB)JOINCOND))
JO6	(THSETQ(THV PROCDATA)(CDR(THV PROCDATA))T T)
	(COND((THV PROCDATA)(GO JO3)))
	(RETURN T)   ))
EXPR)


(DEFPROP INCRELIT
   (LAMBDA(L B)
	(COND((NULL L)B)
	     (T(INCRELIT(CDR L)(CDR B))))  )
EXPR)


(DEFPROP STORPLIB
   (LAMBDA NIL
     (PROG(PRO)
	(COND((NULL COMPI)(ED T)))
	(OUTC @PLIB NIL)
	(SETQ PRO(LIST @DEFPROP PL
	   (APPEND(LIST @THCONSE)
		  (LIST GVARL)
		  (LIST(CAR TAS))
		  (IAS(APPEND TYP STA))
		  (LIST(LIST @THSET @(CAR(THV ANS))(LIST @APPEND @(EVAL(CAR(THV ANS)))
				(LIST @REVERSE(LIST @INSTPROG(LIST @QUOTE PANS)(LIST  @QUOTE GVARL) )))))
		  (OAS TAS))
	   @THEOREM))
	(SPRINT PRO 2 1)
	(PRINT(LIST @THASSERT PL))
	(OUTC NIL NIL)   ))
EXPR)


(DEFPROP IAS
   (LAMBDA(IA)
	(COND((NULL IA)NIL)
	     (T(CONS(LIST @THGOAL(CAR IA)@(THTBF THTRUE))(IAS(CDR IA)))))  )
EXPR)


(DEFPROP INSTPROG
   (LAMBDA(PA VARL)
	(COND((NULL VARL)PA)
	     (T(INSTPROG(SUBST(EVAL(LIST @THV(CAR VARL)))(LIST @THV(CAR VARL))PA)(CDR VARL))))  )
EXPR)



(DEFPROP OAS
   (LAMBDA(TAS)
	(COND((NULL TAS)NIL)
	     (T(CONS(LIST @THASSERT(CAR TAS))(OAS(CDR TAS)))))  )
EXPR)


(DEFPROP GENERALIZE
   (LAMBDA NIL 
      (PROG (TAS TDB CL VN VA PANS TYP STA TEM TEM1 GPAR GVARL)
	(PRINT @IS_THIS_PLAN_USEFUL_ENOUGH_TO_BE_GENERALIZED?*)
	(COND((READ)(SETQ GSWI GANS))
	     (T(GO GE9)))
	(PRINT @DO_YOU_WANT_TO_SEE_THE_GENERALIZED_VERSION?*)
	(COND((READ)(SETQ GGEN T))(T(SETQ GGEN NIL)))
	(SETQ TDB(DBREF(THV DBLITS)(APPEND(THV WASSERTLITS)(THV ASSERTLITS))))
	(SETQ TAS(REVERSE(NETASSERT(THV ASSERTLITS))))
	(SETQ TEM(APPEND TDB TAS))
GE4	(SETQ CL(APPEND(CONSTL(CDAR TEM))CL))
	(SETQ TEM(CDR TEM))
	(COND(TEM(GO GE4)))
	(SETQ GENAL(REVERSE(CDR(REVERSE(CDR (CAR TAS))))))
(PRINT @L45419)(PRINT GOL)(PRINT TDB)(PRINT TAS)	(SETQ GPAR @ALL)
	(PRINT @IS_THIS_A_PROCEDURE_WITHOUT_SIDE_EFFECTS?*)
	(COND((READ)(SETQ GPAR (CDR(REVERSE(CDR(REVERSE GOL)))))))
	(COND((NOT(EQ GPAR @ALL))(SETQ CL GPAR)(SETQ TDB(ELIMLOCALPAR TDB))(SETQ TAS(ELIMLOCALPAR TAS))))
	(SETQ GCON(REVERSE CL))
(PRINT @L45460)(PRINT GANS)(PRINT TDB)(PRINT TAS)
	(SETQ PANS GANS)
	(SETQ VN 0)   (SETQ IGTDB TDB)  (SETQ IGTAS TAS)
	(SETQ GTDB TDB)(SETQ GTAS TAS)(SETQ GVL NIL)(SETQ GTYP NIL)(SETQ GSTA NIL)
GE5	(SETQ VA(LIST @THV(READLIST(APPEND @(V)(EXPLODE(SETQ VN(ADD1 VN)))))))
	(SETQ TDB(SUBST VA(CAR CL)TDB))
	(SETQ TAS(SUBST VA(CAR CL)TAS))
	(SETQ PANS(SUBST VA(CAR CL)PANS))
	(SETQ VA(CADR VA))
	(SETQ GVARL(CONS VA GVARL))
	(SETQ GVL(CONS VA GVL))
	(SETQ GTDB(SUBST VA(CAR CL)GTDB))
	(SETQ GTAS(SUBST VA(CAR CL)GTAS))
	(SETQ GSWI(SUBST VA(CAR CL)GSWI))
	(SETQ CL(CDR CL))
	(COND(CL(GO GE5)))
	(SETQ GENAL(COND((ATOM GTAS)NIL)(T(REVERSE(CDR(REVERSE(CDAR GTAS)))))))
	(SETQ TEM TDB) (SETQ TEM1 GTDB)
GE6	(COND((EQ @R(CAR(REVERSE(CAR TEM))))(SETQ STA(CONS(CAR TEM)STA)))
	     (T(SETQ TYP(CONS(CAR TEM)TYP))))
	(COND((EQ @R(CAR(LAST(CAR TEM1))))(SETQ GSTA(CONS(CAR TEM1)GSTA)))
	     (T(SETQ GTYP(CONS(CAR TEM1)GTYP))))
	(SETQ TEM(CDR TEM))
	(SETQ TEM1(CDR TEM1))
	(COND(TEM(GO GE6)))
	(SETQ TAS(REVERSE TAS))
	(SETQ GTAS(REVERSE GTAS))
(PRINT @L46660)(PRINT TAS)(PRINT TYP)(PRINT STA)
	(STORPLIB)
GE9	(SETQ READY(CONS(CONS(LIST PL GOL ST)(LIST GANS))READY))  ))
EXPR)


(DEFPROP ELIMLOCALPAR
   (LAMBDA(TL)
	(COND((NULL TL)NIL)
	     ((HASGLOB(CDAR TL))(CONS(CAR TL)(ELIMLOCALPAR(CDR TL))))
	     (T(ELIMLOCALPAR(CDR TL))))   )
EXPR)



(DEFPROP HASGLOB
   (LAMBDA(LI)
	(COND((OR(NULL LI)(EQ(CAR LI)@R))T)
	     ((AND(NOT(ATOM(CAR LI)))(NOT(NUMBERP(CAAR LI))))(AND(HASGLOB(CAR LI))(HASGLOB(CDR LI))))
	     ((NOT(MEMBER(CAR LI)CL))NIL)
	     (T(HASGLOB(CDR LI))))  )
EXPR)



(DEFPROP DBREF
   (LAMBDA(DB AS)
      (PROG(TD1 TD2)
	(SETQ TD1(CARDBLIT DB))
	(SETQ TD1(NONREDUN(REVERSE TD1)))
DB2	(COND((NOT(ELASSOC(CAR TD1)AS))
	      (SETQ TD2(CONS(CAR TD1)TD2))))
	(SETQ TD1(CDR TD1))
	(COND(TD1(GO DB2)))
	(RETURN TD2)   ))
EXPR)




(DEFPROP ELASSOC
   (LAMBDA(L AL)
	(COND((NULL AL)NIL)
	     ((EQUAL L(CAAR AL))(CADAR AL))
	     (T(ELASSOC L(CDR AL))))  )
EXPR)




(DEFPROP NETASSERT
   (LAMBDA(TA1)
	(COND((NULL TA1)NIL)
	     ((THVAL @(THGOAL(THEV(CAAR TA1))(THTBF FILTERAX))THALIST)
	      (CONS(CAAR TA1)(NETASSERT(CDR TA1))))
	     (T(NETASSERT(CDR TA1))))    )
EXPR)



(DEFPROP CONSTL
   (LAMBDA(TX)
	(COND((NULL TX)NIL)
	     ((EQ @R(CAR TX))NIL)
	     ((MEMBER(CAR TX)CL)(CONSTL(CDR TX)))
	     ((NOT(ATOM(CAR TX)))(APPEND(CONSTL(CDAR TX))(CONSTL(CDR TX))))
	     (T(CONS(CAR TX)(CONSTL(CDR TX))))))
EXPR)



(DEFPROP CARDBLIT
   (LAMBDA(DBL)
	(COND((NULL DBL)NIL)
	     (T(APPEND(CARDBLIT1(CAR DBL))(CARDBLIT(CDR DBL))))))
EXPR)


(DEFPROP CARDBLIT1
   (LAMBDA(TDBL)
	(COND((NULL TDBL)NIL)
	     ((ATOM(CAR TDBL))(CARDBLIT1(CDR TDBL)))
	     (T(CONS(CAADAR TDBL)(CARDBLIT1(CDR TDBL))))))
EXPR)


(DEFPROP NONREDUN
   (LAMBDA(DBL)
      (PROG(NRL PDBL)
	(SETQ PDBL DBL)
NO2	(COND((NOT(MEMBER(CAR PDBL)NRL))
	      (SETQ NRL(CONS(CAR PDBL)NRL))))
	(SETQ PDBL(CDR PDBL))
	(COND(PDBL(GO NO2)))
	(RETURN(REVERSE NRL))   ))
EXPR)



(DEFPROP OUTANS
   (LAMBDA NIL
      (PROG(GTYP1 GTYP1 GTAS1 IGTYP IGSTA IGTDB1 COMLST CLST)
	(TERPRI)
	(PRINT @THE_GOAL_)(PRINC (REVERSE(CDR(REVERSE GOL))))(PRINC @_IS_ATTAINABLE_BY_THE_FOLLOWING_PROGRAM:)
	(TERPRI)(TERPRI)
(COND((ATOM PL)(PRINT PL))(T(PRINT(CAR PL))))
(PRINC(REVERSE(CDR(REVERSE(CDR GOL)))))
	(COND((NULL GSWI)(GO OU41)))
	(SETQ IGTDB1 IGTDB)
OU1	(COND((EQ @R(CAR(LAST(CAR IGTDB1))))(SETQ IGSTA(CONS(CAR IGTDB1)IGSTA)))
	     (T(SETQ IGTYP(CONS(CAR IGTDB1)IGTYP))))
	(SETQ IGTDB1(CDR IGTDB1))
	(COND(IGTDB1(GO OU1)))
	(TERPRI)
OU12	(PRINC(CAAR IGTYP))  (PRINC(CDAR IGTYP))  (PRINC @;)
	(SETQ IGTYP(CDR IGTYP))
	(COND(IGTYP(GO OU12)))
	(PRINT @COMMENT)(PRINT @INPUT_CONDITIONS:)(TERPRI)
	(OUTCONDI IGSTA)
	(PRINT @OUTPUT_CONDITIONS:)(TERPRI)
	(OUTCONDI IGTAS)
	(PRINC @;)
OU41	(COND((THV ASSL)(PRINT @COMMENT)
              (PRINT @THIS_PROGRAM_RELIES_ON_THE_FOLLOWING_ASSUPTIONS:)(PRINT(THV ASSL))(PRINC @;)))
    	(COND((THV COMMENTLIST)(PRINT @COMMENT))
             (T(GO OU02)))
	(SETQ CLST(THV COMMENTLIST))
OU4	(COND((NULL CLST)(PRINC @;)(GO OU02)))
	(TERPRI)
	(SETQ COMLST(CAR CLST))
	(THSETQ CLST(CDR CLST)T T)
OU5	(COND((NULL COMLST)(GO OU4)))
	(PRINC(CAR COMLST))(PRINC @" ")
	(SETQ COMLST(CDR COMLST))
	(GO OU5)
OU02	(SETQ INDENT NIL)
   	(TSLPLAN GANS)
	(COND(STAT(TERPRI)
                  (PRINT THME)(PRINC @__RULES_ENTERED)(PRINT THMS)(PRINC @__RULES_SUCCESSFUL)))
	(TERPRI)
	(COND((OR(NULL GSWI)(NULL GGEN))(RETURN T)))
	(SETQ GTYP1 GTYP) (SETQ GSTA1 GSTA) (SETQ GTAS1 GTAS)
	(PRINT @THIS_PLAN_HAS_ALSO_BEEN_GENERALIZED_AND_RESIDES_IN_THE)
	(PRINT @LIBRARY_IN_THE_FORM:)
	(TERPRI)
(COND((ATOM PL)(PRINT PL))(T(PRINT(CAR PL))))
(PRINC GENAL)
(TERPRI)
OU3	(PRINC(CAAR GTYP1))(PRINC(CDAR GTYP1))
	(PRINC @;) 
	(SETQ GTYP1(CDR GTYP1))
	(COND(GTYP1(GO OU3)))
	(PRINT @COMMENT)
	(PRINT @INPUT_CONDITIONS:)(TERPRI)
	(OUTCONDI GSTA1)
	(PRINT @OUTPUT_CONDITIONS:)(TERPRI)
	(OUTCONDI GTAS1)
	(PRINC @;)
   	(TSLPLAN GSWI) (TERPRI)  ))
EXPR)



(DEFPROP OUTCONDI
   (LAMBDA(CC)
      (PROG(LCC)
	(COND((NULL CC)(PRINC @NONE)(RETURN T)))
	(SETQ LCC CC)
OU00	(PRINC(CAAR LCC))
	(COND((EQ @R(CAR(LAST(CAR LCC))))
	      (PRINC(REVERSE(CDR(REVERSE(CDAR LCC))))))
	     (T(PRINC(CDAR LCC))))
	(SETQ LCC(CDR LCC))
	(COND(LCC(PRINC @∧)(GO OU00)))
	(RETURN T)  ))
EXPR)





(DEFPROP PROCJOIN
   (LAMBDA NIL
      (PROG(JC)
	(COND((NOT(SETQ JC(FINDCOND JOINCOND)))(RETURN T)))
	(SETQ SSW T)
	(SETQ JCFC(TESTJOIN JC))
	(SETQ SSW NIL)
	(COND((NULL JCFC)(RETURN T)))
	(RETURN NIL)  ))
EXPR)


(DEFPROP FINDCOND
   (LAMBDA(JOC)
	(COND((NULL JOC)NIL)
	     ((MEMBER PL(CAAR JOC))(CADAR JOC))
	     (T(FINDCOND(CDR JOC)))))
EXPR)

(DEFPROP TESTJOIN
   (LAMBDA(JC)
	(COND((NULL JC)NIL)
	     ((THVAL @(THGOAL(THEV(CAR JC)))THALIST)
	      (TESTJOIN(CDR JC)))
	     (T(CAR JC)))   )
EXPR)

(DEFPROP STEPREF
   (LAMBDA(OPN ARGL GL)
      (PROG(ST)
	(COND((AND(THV WF)(THASVAL(THV FT)))(RETURN T)))
        (SETQ ST(READLIST(APPEND @(S T A T)(EXPLODE(SETQ SN(ADD1 SN))))))
        (SAVESTATE ST)
        (SETQ LIFOL(CONS(LIST(CONS OPN ARGL)GL ST)LIFOL))
        (THSETQ(THV ASSL)(CONS OPN(THV ASSL)))
        (RETURN T)  ))
EXPR)

(DEFPROP POPN
   (LAMBDA NIL
      (PROG(N)
        (SETQ N(LENGTH(THV ASSL)))
PO2     (COND((ZEROP N)(RETURN T)))
        (SETQ N(SUB1 N))
        (SETQ LIFOL(CDR LIFOL))
        (GO PO2)   ))
EXPR)


(DEFPROP SUBGOAL
   (LAMBDA (L)
      (PROG(JCFC PL GOL ST PREDLIST LGANS LCT INDENT STAT THME THMS GANS RES FILENAME COMPI GENAL LIBFIT
            PVARLIST GSWI GTDB GTAS GVL GCON GSTA GTYP GGEN IGTDB IGTAS FUNDEFLIST P1A P2A P3A P4A P5A)
	(CSYM NF00)
SU0	(COND((EQ T(CAR L))(GO SU40)))
	(COND((AND(NOT(NULL L))(NOT(EQ @DSK:(CAR L))))(SETQ FILENAME(CAR L))(GO SU10)))
	(COND((NULL COMPI)(DSKIN COMPR)(ED T)(SETQ COMPI T)))
	(COMP L)
SU10	(EVAL(LIST @DSKIN FILENAME))
	(COND((AND(NOT(NULL L))(NOT(EQ @DSK:(CAR L))))(RESTOREPROP)(REMPROP @RESTOREPROP @EXPR)))
	(OUTC(OUTPUT DSK: INIT)T)
	(THDUMP)
	(OUTC NIL)
	(OUTC(OUTPUT PLIB DSK: PLIB)NIL)
	(OUTC NIL NIL)
	(SETQ ST @INIT)
SU12	(PRINT @SUBMIT_GOAL*)
	(SETQ GOL(READ))
	(SETQ LIBFIT NIL)
	(SETQ PL(READLIST(APPEND @(P R O C)(EXPLODE(SETQ PN(ADD1 PN))))))
	(PRINT @DO_YOU_WANT_TO_TRY_USING_THE_PROGRAM_LIBRARY?)
	(COND((READ)(SETQ LIBFIT T)(DSKIN PLIB)))
SU13	(PRINT @DO_YOU_HAVE_ANY_ADVICE?*)
	(COND((READ)(ADVICESYS)))
SU15	(SETQ THME 0)(SETQ THMS 0)
	(THVSETQ(THV COMMENTLIST)NIL)
  	(SETQ THSTEPT @(STEPT))
	(COND((AND(GET(CAR GOL)@FLUENT)(NOT(EQ @R(CAR(LAST GOL)))))(SETQ GOL(APPEND GOL(LIST @R)))))
	(SETQ RES(THVAL(LIST @THGOAL GOL(LIST @THTBF @THTRUE))THALIST))
	(SETQ THSTEPT NIL)
	(COND((NULL RES)(GO SU17)))
	(COND((PROCJOIN)(GO SU16)))
	(PRINT @THE_JOIN_CONDITION_)(PRINC JCFC)(PRINC @_FAILED!)
	(PRINT @HENCE_THE_PROCEDURE_IN_ITS_PRESENT_FORM_CANNOT_BE_USED)
	(PRINT @DO_YOU_WANT_TO_EXTEND_THE_PROCEDURE_)(PRINC PL)(PRINC @_TO_SATISFY_)(PRINC JCFC)(PRINC @*)
	(COND((READ)(SETQ GOL JCFC)(SETQ JCFC NIL)(GO SU13)))
	(GO SU20)
SU16	(COND((THV PROCDATA)(CJOINCOND)))
	(COND((NULL GANS)(PRINT @GOAL_TRUE_IN_PRESENT_WORLD!)(TERPRI)(GO SU20)))
	(PRINT @DO_YOU_WANT_TO_OPTIMIZE_THE_PROGRAM?*)
	(COND((READ)(SETQ GANS(OPTIM GANS))))
	(GENERALIZE)
	(GO SU18)
SU17	(PRINT @THE_GOAL_FAILED!__DO_YOU_WANT_TO_TRY_AGAIN_WITH_MORE_ADVICE?*)
	(COND((READ)(ADVICESYS)(GO SU15)))
	(GO SU20)
SU18	(OUTANS)
(PRINT PL)
	(EVAL(LIST @OUTC(LIST @OUTPUT @DSK: (COND((ATOM PL)PL)(T(CAR PL))))T))
	(OUTANS)
	(OUTC NIL)
        (COND((NULL(THV ASSL))(GO SU20)))
        (PRINT @DO_YOU_WANT_TO_DO_STEPWISE_REFINEMENT:)
        (COND((NULL(READ))(POPN)(GO SU20)))
SU19    (SETQ PL(CAR LIFOL))
        (SETQ LIFOL(CDR LIFOL))
        (GO SU25)
SU20	(COND((NULL FIFOL)(GO SU28)))
	(PRINT @DO_YOU_WANT_TO_DO_CONTINGENCY_PLANNING?*)
	(COND((NULL(READ))(GO SU30)))
	(THSETQ(THV DBLITS)NIL T T)
	(THSETQ(THV ASSERTLITS)NIL T T)
	(PRINT @WHAT_IS_YOUR_PREFERENCE?__IF_NONE_TYPE_NIL*)
SU22	(SETQ PL(READ))
(PRINT @L57225)(PRINT PL)
	(COND((NULL PL)(SETQ PL(CAR FIFOL))(PRINT NIL)(PRINT PL)(SETQ FIFOL(CDR FIFOL)))
	     ((SETQ PL(ASSOC PL FIFOL))(PRINT T)(PRINT PL)(SETQ FIFOL(DELAD1(CAR PL)FIFOL)))
	     (T(PRINT @NO_SUCH_PROC___TRY_AGAIN*)(GO SU22)))
SU25	(SETQ GOL(CADR PL))
	(COND((EQUAL(LAST GOL)@(R))(SETQ GOL(REVERSE(CDR(REVERSE GOL))))))
	(THFLUSH THASSERTION THERASING THCONSE)
(PRINT @L57525)(PRINT PL)
	(SETQ ST(CADDR PL))
(PRINT @L57575)(PRINT ST)
	(PRINT @TRYING___)(PRINC PL)
	(EVAL(LIST @DSKIN ST))
	(SETQ PL(CAR PL))
	(SETQ GANS NIL)
	(THVSETQ(THV PROCDATA)NIL)
	(THVSETQ(THV PASSUM)NIL)
        (THVSETQ(THV ASSL)NIL)
	(THVSET(CAR(THV ANS))NIL)
(THSETQ(THV O1)@THUNASSIGNED)
	(SETQ LCT NIL)(SETQ LGANS NIL)
	(GO SU13)
SU28    (COND((NULL(THV ASSL))(GO SU30)))
        (PRINT @DO_YOU_WANT_TO_DO_STEPWISE_REFINEMENT:)
        (COND((NULL(READ))(GO SU30)))
        (GO SU19)
SU30	(COND(JCFC(PRINT @INITIAL_STATE_REENTERED)(GO SU40)))
	(SETQ GANS NIL)
	(SETQ LCT NIL)(SETQ LGANS NIL)
	(PRINT @DO_YOU_WANT_TO_CONTINUE_FROM_THE_PRESENT_STATE_OF_THE_WORLD?)
	(COND((READ)(GO SU12)))
SU40	(THFLUSH THASSERTION THERASING THCONSE)
	(THSETQ(THV DBLITS)NIL T T)
	(THSETQ(THV ASSERTLITS)NIL T T)
	(DSKIN INIT)
	(SETQ ST @INIT)
	(THVSETQ(THV PROCDATA)NIL)
	(THVSET(CAR(THV ANS))NIL)
	(THVSETQ(THV PASSUM)NIL)
        (THVSETQ(THV ASSL)NIL)
	(GO SU12)
))
FEXPR)